\begin{tabbing}
$\forall$$k$:Knd, $T$, $A$, $B$:Type, $l$:IdLnk, $x$, ${\it tg}$:Id, $f$:($A$$\rightarrow$$B$$\rightarrow$$T$), $c$:($A$$\rightarrow$$B$$\rightarrow\mathbb{B}$).
\\[0ex](($\uparrow$isrcv($k$))
\\[0ex]$\Rightarrow$ (destination(lnk($k$)) = source($l$) $\in$ Id \& ((lnk($k$) = $l$) $\Rightarrow$ ($T$ = $B$ \& tag($k$) = ${\it tg}$))))
\\[0ex]$\Rightarrow$ Normal($A$)
\\[0ex]$\Rightarrow$ Normal($T$)
\\[0ex]$\Rightarrow$ Normal($B$)
\\[0ex]$\Rightarrow$ $\vdash$${\it es}$. $k$\=(v:$B$) sends\+
\\[0ex]$f$($x$:$A$,v) on
\\[0ex]$l$ tagged with ${\it tg}$:$T$
\\[0ex]provided $c$($x$,v)
\-
\end{tabbing}